<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
<title>PrettyProlog implementation details - the Engine class</title>
<meta http-equiv="content-type" content="text/html; charset=iso-8859-1">
<meta name="generator" content="Emacs">
<style type="text/css">
@import url("../style.css");
</style>
</head>
<body>
<div id="container">
    <div id="header">
        <h1>PrettyProlog - the Engine class</h1>
    </div>
    <div id="content">
	<p align="left">
	  The Engine class is the core class of the PrettyProlog system. We're going to examine it in close detail.<br /><br />
	  To perform its operations, the Engine needs three objects:
	  <ul>
            <li>a <b>Unifier</b>, that is used to perform unification of terms</li>
	  <li>a <b>Theory</b> containing user-specified clauses.<br />
              Since it is possible to attach listeners to the Theory, the Engine must maintain a reference to the same Theory during its entire life time. So every method of Engine that operates on theories, such as loadTheory(), modifies the current Theory instead of creating a new one. A defaultTheory() method is also provided, which is used to obtain the &quot;default&quot; theory (the one the engine begins with). By now it just returns a new, empty Theory, but it can be overriden so that certain additional clauses are present in every loaded Theory and aren't deleted when the Engine.resetTheory() method is called.</li>
	  <li>a <b>Stack</b>. The Stack also can have listeners, so what previously stated for Theory applies to it, too.</li></ul>
	  A reference to each of these objects can be obtained by calling the appropriate method. Of course, modifying these objects during goal solving might produce unwanted results such as wrong solutions, infinite recursion, or other non-predictable bugs. You have been warned.<br />
	  The engine is controlled by the solve(), continueSolving(), pause(), and abort() methods. The first initializes the Stack and some internal flags, then calls continueSolving(). This is the main method of the engine: it solves goals using the Stack, Theory, and Unifier. continueSolving() stops only when all solutions have been found, or when either the pause() or abort() method are called. Both these methods stop the solving process, but abort() also resets the engine state so that a subsequent call to continueSolving() won't do anything.<br />
	  The programmer can add EngineListeners to an Engine. These will be notified every time a solution is found, or any of the four main methods (solve(), continueSolving(), pause(), or abort()) is called. Input/output, on the other hand, is managed by a separate class, Engine.IOManager, which has the obvious input(), output(), and error() methods. Unlike listeners, there can be only one IOManager associated with the Engine at a certain time; however, if needed, it is quite trivial to write an IOManager that does input/output to and from any number of different sources.
	<br />
	</p>
	<p align="left">
	  <h4>The solving algorithm.</h4>
	  Here is the solving algorithm in detail, first as studied in the course, then how it has been modified to suit a closer-to-the-real-world Prolog implementation. The symbol * has been used as the composition operator, while / is the application of a substitution.
<pre>
-- Algorithm studied in the course --

Input: a program P (ordered set of clauses) and a goal G (list of terms)
Output: every substitution S such that G/S is an instance of G obtained from P,
        or failure if no such S exists.
Algorithm:
Let R = G, q = {empty substitution}, Fail = false:
  Initialize a stack S with (R, q, 0). 
  While S is not empty do:
    Let (R, q, j) the top of S:
      If R is not empty then:
	choose a subgoal A : R = [A|G'].
	choose a clause c_i = A' :- A1 , ..., An from P 
	(renaming variables) such that:
	  i is the minimum index in the theory that is greater than j, and
          it exists s = mgu(A, A'), a substitution that unifies A and A'.
	If such A and c_i exist then:
	  set R' = [A1 ,..., An|G']/s.
	  update the top of S so that j gets replaced by i.
	  push (R', q*s, 0) onto S
	Else set Fail = true.
      Else print q and set Fail = true.
      If Fail = true then:
	pop from S and set Fail = false.
  End.
If no solutions were printed print failure.

-- Algorithm implemented in PrettyProlog (simplified) --

Input: a Theory T, a Unifier U and a Goal (list of Terms) G
Output: every substitution S such that G/S is an instance of G obtained from P,
        or failure if no such S exists.

Algorithm: 
Let print(X): return the printed representation of X.

Let R = G, q = {empty substitution}, Fail = false, CutMark = 0:
  Initialize a stack S with (R, q, 0, null, CutMark).
  While S is not empty do:
    If Fail = true then:
      Pop from S.
      Set Fail = False.
    If S is empty then return.     
    Let (R, q, j, str, mark) the top of S:
      If R is not empty then:
	choose the first subgoal A of R = [A|G'].
	If A is not a system predicate then:
	  choose a clause c_i = A' :- A1 , ..., An from T
	  (renaming variables) such that:
	     i is the minimum index in the theory that is greater than j, and
             it exists s = U.unify(A, A'),
             a substitution that unifies A and A'.
	  If such A and c_i exist then:
	    If c_i contains !:
              Set CutMark = CutMark + 1.
              Update the top of S so that it contains the new CutMark.
            Set R' = [A1 ,..., An|G']/s.
            Set q = q*s.
	    update the top of S so that j gets replaced by i.
	    push (R', q, 0, print(c_i), CutMark) onto S.
	  Else set Fail = true.
        Else:
          update the top of S so that j gets replaced by j + 1.
          If j = 1 OR A is a backtrackable syspred then:
            Let effect = Call a:
              Set Fail = effect.Fail.
              Set q = effect.Substitution.
          Else Set Fail = true.
          If Fail = false:
            Set R' = R/q.
            push (R', q, 0, print(A), CutMark) onto S.
      Else:
        Set Fail = true.
        Output q.
  End.
</pre>
	</p>
    </div>
    <div id="footer"><a href="../index.html">General info</a> | <a href="../javadoc/index.html">Javadocs</a> | <a href="index.html">Implementation details</a></div>
</div>
</body>
</html>